poss:(ES{i}Prop{i'}), R:(possible-event{i:l}(poss)possible-event{i:l}(poss)Prop{i'}).
(Trans a,b:possible-event{i:l}(poss). R(a,b))
 (P:(possible-event{i:l}(poss)Prop{i'}), e:possible-event{i:l}(poss).
 (es-knows{i:l}
 (es-knows(poss; R; P; e)
 ( es-knows{i:l}
 ( es-knows(poss; R; (e.es-knows{i:l}(poss; R; P; e)); e)) 

latex

Definitions	x:AB(x), x:A. B(x), Trans x,y:T. E(x;y), x:AB(x), PossibleEvent(poss), f(a), t  T, P  Q, Type, Prop, ES, x,y. t(x;y), K(P)@e
Lemmas	trans wf, possible-event wf, event system wf